   Exception: (10) cons((ci, alpha_1_), pri(lst, [pri(hash, [ctxm(_G1073, _G1074, _G1075, _G1076, i_bsn)]), ctxm(_G1082, _G1083, _G1084, _G1085, (ip, umc1)), ctxm(_G1091, _G1092, _G1093, _G1094, (c, d_1)), ctxm(_G1100, _G1101, _G1102, _G1103, (c, d_2)), ctxm(_G1109, _G1110, _G1111, _G1112, (c, d_3))])) ?    Exception: (8) transvalid((ci, alpha_1_), (ci, alpha_1_), tm(st, pri(lst, [pri(hash, [ctxm(alpha_1_, u, bsn, i_bsn, i_bsn)]), ctxm(alpha_1_, umc, ip, (ip, umc1), (ip, umc1)), ctxm(alpha_1_, u, (d, all, 1), (i, d_1), (c, d_1)), ctxm(alpha_1_, u, (d, ..., ...), (i, d_2), (c, d_2)), ctxm(alpha_1_, u, (..., ...), (..., ...), (..., ...))]))) ? 
knows((ci,alpha_1_),ctxm(alpha_1_,umc,ip, (ip,umc1), (ip,umc1))).
knows((ci,alpha_1_),ctxm(alpha_1_,ci,ip, (ip,ci), (ip,ci))).
knows((ci,alpha_1_),pri(lst,[pri(hash,[ctxm(alpha_1_,u,bsn,i_bsn,i_bsn)]),ctxm(alpha_1_,u, (d,all,1), (i,d_1), (c,d_1)),ctxm(alpha_1_,u, (d,all,2), (i,d_2), (c,d_2)),ctxm(alpha_1_,u, (d,all,3), (i,d_3), (c,d_3))])).
knows((umc1,alpha_1_),pri(lst,[pri(hash,[ctxm(alpha_1_,u,bsn,i_bsn,i_bsn)]),ctxm(alpha_1_,u, (d,all,1), (i,d_1), (c,d_1)),ctxm(alpha_1_,u, (d,all,2), (i,d_2), (c,d_2)),ctxm(alpha_1_,u, (d,all,3), (i,d_3), (c,d_3))])).
knows((umc1,s),ctxm(dot,ps,ip, (ip,ps), (ip,ps))).
knows((umc1,s),ctxm(dot,umc1,ip, (ip,umc1), (ip,umc1))).
knows((umc1,s),ctxm(dot,umc2,ip, (ip,umc2), (ip,umc2))).
knows((umc1,s),ctxm(dot,umc3,ip, (ip,umc3), (ip,umc3))).
knows((umc1,s),ctxm(dot,ci,ip, (ip,ci), (ip,ci))).
knows((umc1,s),ctxm(dot,r,ip, (ip,r), (ip,r))).
knows((umc1,s),ctxm(kappa_,u,bsn,i_bsn,i_bsn)).
knows((umc1,s),ctxm(kappa_,u,d_1, (i,d_1), (c,d_1))).
knows((umc1,s),ctxm(kappa_,u,d_2, (i,d_2), (c,d_2))).
knows((umc1,s),ctxm(kappa_,u,d_3, (i,d_3), (c,d_3))).
knows((umc1,s),ctxm(kappa_,u,d_4, (i,d_4), (c,d_4))).
knows((umc1,s),pri(lst,[ctxm((umc1,alpha_1_),u,bsn,i_bsn,i_bsn),pri(hash,[ctxm((umc1,alpha_1_),u,bsn,i_bsn,i_bsn)])])).
knows((umc2,s),ctxm(dot,ps,ip, (ip,ps), (ip,ps))).
knows((umc2,s),ctxm(dot,umc1,ip, (ip,umc1), (ip,umc1))).
knows((umc2,s),ctxm(dot,umc2,ip, (ip,umc2), (ip,umc2))).
knows((umc2,s),ctxm(dot,umc3,ip, (ip,umc3), (ip,umc3))).
knows((umc2,s),ctxm(dot,ci,ip, (ip,ci), (ip,ci))).
knows((umc2,s),ctxm(dot,r,ip, (ip,r), (ip,r))).
knows((umc2,s),ctxm(mu_,u,bsn,i_bsn,i_bsn)).
knows((umc2,s),ctxm(mu_,u,d_5, (i,d_5), (c,d_5))).
knows((umc2,s),ctxm(mu_,u,d_6, (i,d_6), (c,d_6))).
knows((umc2,s),ctxm(mu_,u,d_7, (i,d_7), (c,d_7))).
knows((umc2,s),ctxm(mu_,u,d_8, (i,d_8), (c,d_8))).
knows((umc2,s),ctxm(dot,umc2,dom, (dom,umc2), (dom,umc2))).
knows((ci,s),ctxm(dot,ps,ip, (ip,ps), (ip,ps))).
knows((ci,s),ctxm(dot,umc1,ip, (ip,umc1), (ip,umc1))).
knows((ci,s),ctxm(dot,umc2,ip, (ip,umc2), (ip,umc2))).
knows((ci,s),ctxm(dot,umc3,ip, (ip,umc3), (ip,umc3))).
knows((ci,s),ctxm(dot,ci,ip, (ip,ci), (ip,ci))).
knows((ci,s),ctxm(dot,r,ip, (ip,r), (ip,r))).
knows((ci,s),ctxm(dot,r,dom, (dom,r,beta_1_), (dom,r,beta_1_))).
knows((ci,s),ctxm(dot,r,dom, (dom,r,beta_2_), (dom,r,beta_2_))).
knows((ci,s),pri(lst,[pri(hash,[ctxm((ci,alpha_1_),u,bsn,i_bsn,i_bsn)]),ctxm((ci,alpha_1_),umc,ip, (ip,umc1), (ip,umc1)),ctxm((ci,alpha_1_),u, (d,all,1), (i,d_1), (c,d_1)),ctxm((ci,alpha_1_),u, (d,all,2), (i,d_2), (c,d_2)),ctxm((ci,alpha_1_),u, (d,all,3), (i,d_3), (c,d_3))])).
knows((r,s),ctxm(dot,ps,ip, (ip,ps), (ip,ps))).
knows((r,s),ctxm(dot,umc1,ip, (ip,umc1), (ip,umc1))).
knows((r,s),ctxm(dot,umc2,ip, (ip,umc2), (ip,umc2))).
knows((r,s),ctxm(dot,umc3,ip, (ip,umc3), (ip,umc3))).
knows((r,s),ctxm(dot,ci,ip, (ip,ci), (ip,ci))).
knows((r,s),ctxm(dot,r,ip, (ip,r), (ip,r))).
knows((r,s),ctxm(beta_1_,u,d_9, (i,d_9), (c,d_9))).
knows((r,s),ctxm(beta_2_,u,d_10, (i,d_10), (c,d_10))).
